feat(scripts): kernel-level axiom sweep with committed regression baseline - #300

scripts/AxiomSweep.lean (18)

• def buildEntries (roots : Array Name) : CoreM (Array Entry × Nat)
• def currentBaseline (entries : Array Entry) : Baseline where
• def dedupSort (a : Array String) : Array String
• def defaultRoots : Array Name
• def isReportable (n : Name) : Bool
• def isStandard (a : String) : Bool
• def kindOf : ConstantInfo → String
• def neverAllowlistable (a : String) : Bool
• def nonstandardOf (e : Entry) : Array String
• def normalizeAxiomName (s : String) : String
• def parseArgs : List String → Config → Except String Config
• def reportNeverAllowlistable (cur : Baseline) : IO Bool
• def runCheck (cur : Baseline) (basePath : String) : IO UInt32
• def sorryAxName : String
• def standardAxioms : List Name
• partial def collect (env : Environment) (stack : List Name) (gray : Std.HashSet Name)
• partial def repair (env : Environment) (order : Array Name)
• unsafe def main (args : List String) : IO UInt32

scripts/AxiomSweep.lean (4)

• def currentBaseline (entries : Array Entry) : Baseline where (L229)
• def runCheck (cur : Baseline) (basePath : String) : IO UInt32 (L258)
• def runCheck (cur : Baseline) (basePath : String) : IO UInt32 (L259)
• partial def repair (env : Environment) (order : Array Name) (L146)

No findings.

• .github/workflows/lean_action_ci.yml: A new 'Axiom sweep' CI step runs lake exe axiomsweep --check to verify that no unwanted axioms are introduced in the project. This step is placed between the timing report generation and the fail-on-warnings step, adding an additional validation layer to the build pipeline.
• AGENTS.md: Added a new workflow step (step 6) to AGENTS.md instructing contributors to run lake exe axiomsweep --check when filling or adding a sorry, and to update the axiom baseline with --update-baseline if the change is intentional. This documents the project's practice of tracking axiom usage and ensuring that sorry additions are properly accounted for in the axiom baseline, with a note that native-compiler trust is never baselineable.
• docs/wiki/generated-files.md: Added a new row to the table of generated files in docs/wiki/generated-files.md documenting scripts/axiom_baseline.json. This file is a generated and committed kernel-level axiom/sorry regression baseline, regenerated via lake exe axiomsweep --update-baseline after a lake build. It is checked by an enforcing axiom-sweep CI step, and the description notes that native-compiler trust cannot be baselined.
• docs/wiki/quickstart.md: Adds a dedicated sub-section explaining how to use lake exe axiomsweep --check for kernel-level axiom/sorry accounting across the CompPoly.* library, including baseline management via --update-baseline and CI enforcement in lean_action_ci.yml (line added to the CI description). Also appends lake exe axiomsweep --check to the list of direct debugging commands near the end of the file.
• lakefile.lean: Added a new lean_exe target named axiomsweep with srcDir := "scripts", root := AxiomSweep, and supportInterpreter := true. This executable performs kernel-level axiom/sorry accounting against a committed regression baseline (scripts/axiom_baseline.json). It runtime-imports the built CompPoly oleans, so it must be run after lake build`.
• scripts/AxiomSweep.lean: Added scripts/AxiomSweep.lean, a new script that performs whole-library kernel-level axiom and sorry accounting for CompPoly.* modules. It computes the transitive axiom dependency set for every swept declaration via a DFS (collect) and a fixpoint propagation (repair), supporting four modes: bare summary, writing a full JSON report (--out), checking against a committed baseline (--check), and updating that baseline (--update-baseline). Key definitions include Entry, NonstandardEntry, and Baseline structures; helper functions normalizeAxiomName and dedupSort for robust name handling; reportNeverAllowlistable to reject native-compiler trust axioms; and runCheck which compares current taint sets to the baseline and reports regressions or resolutions.
• scripts/README.md: The README now documents the new AxiomSweep.lean tool (invoked via lake exe axiomsweep), which performs kernel-level axiom/sorry regression checking against a committed baseline (axiom_baseline.json). A brief usage line lake exe axiomsweep --check was added to the script list, and the Script Inventory section gained a detailed sub-section describing the tool's modes (--check, --update-baseline, --out), its source from the built .olean environment, and its rejection of bare and native-compiler trust.
• 1 file(s) filtered as noise (lockfiles, generated, or trivial): scripts/axiom_baseline.json